es:ES, ds:x:Id fp Type, T:Type, i:Id, f:(State(ds)T).
(x, y:T. Dec(x = y))
 (x:Id. vartype(i;x)  ds(x)?Top)
 e'@i.
 (e<e'. f((state when e)) = f((state when e')))
  (e:E.
  ((e <loc e')
  (& f((state when e)) = f(state after e)
  (& & (e'':E. (e <loc e'')  e''  e'   f((state when e'')) = f((state when e'))  T)) 

latex

Definitions

Dec(P), P  Q, e@i. P(e), state after e, 1of(t), a:A fp B(a), ES, (state when e), state@i, State(ds), P  Q, pred(e), vartype(i;x), f(x)?z, x. t(x), IdDeq, Top, b, , first(e), Prop, Id, loc(e), A, P  Q, False, P  Q, e<e'. P(e), x:A. B(x), A & B, P & Q, e  e' , (e <loc e'), E, x:A. B(x), t  T, T, True, {T}, SQType(T)

Lemmas

es-axioms, Id sq, es-state wf, equal functionality wrt subtype rel, state-after-pred, and functionality wrt iff, cand functionality wrt iff, exists functionality wrt iff, or functionality wrt iff, es-pred-locl, implies functionality wrt iff, all functionality wrt iff, es-le-iff, alle-lt wf, true wf, squash wf, es-loc-pred, es-E wf, es-loc wf, Id wf, es-first wf, assert wf, not wf, top wf, id-deq wf, fpf-cap wf, es-vartype wf, es-pred wf, es-locl-iff, es-le-loc, subtype rel self, subtype rel dep function, es-state-when wf, es-le wf, es-locl wf, es-state-after wf, alle-at-iff, event system wf, fpf wf, decl-state wf, decidable wf